Section: New Results

Verification of distributed algorithms in the Heard-Of model

Participants : Henri Debrat, Stephan Merz.

Distributed algorithms are often quite subtle, both in the way they operate and in the assumptions required for their correctness. Formal models are important for unambiguously understanding the hypotheses and the properties of a distributed algorithm. We focus on the verification of round-based algorithms for fault-tolerant distributed systems expressed in the Heard-Of model of Charron-Bost and Schiper [26] , for which we had already proved a reduction theorem in previous work.

In 2011, we have extended our previous results to the case of Byzantine errors where values may be received that do not correspond to those that should have been computed by the sender process (for example because of an intermittent fault in the sender process, a malicious process, or a value-changing error in the transmission channel). We have formalized a corresponding extension of the Heard-Of model in Isabelle/HOL, and have verified three Byzantine Consensus algorithms (EIG, ATE and UTE) within this framework. These results have been presented at SSS 2011 [9] .